\documentclass[xcolor=dvipsnames,mathserif,svgnames,11pt]{beamer}

% for a handout:
%
%\documentclass[handout,11pt]{beamer}
%
%\usepackage{pgfpages}
%\pgfpagesuselayout{2 on 1}[letterpaper,border shrink=5mm]


\usepackage{diagrams}
\usepackage{listings}
\usepackage{proof}
\lstdefinelanguage{MyHaskell}
{alsoletter={+,|,->, =, ::}, morekeywords={+,|,->, =, ::, data, Int, max, case, of}
}


\lstdefinelanguage{MyLambda}
{alsoletter={\., |, ->, = }, morekeywords={=,|, -> ,\., lam , fix, case, of}}


%\lstset{language=MyHaskell, keywordstyle=\color{scyan},basicstyle=\ttfamily}

\definecolor{syellow}{RGB}{181,137,0}
\definecolor{scyan}{RGB}{42,161,152}

\DefineNamedColor{named}{MyBlue}{RGB}{38,139,210}
\DefineNamedColor{named}{Base3}{RGB}{253,246,227}
\DefineNamedColor{named}{Base00}{RGB}{101,123,131}
\newcommand{\yemph}[1]{\colorbox{yellow}{#1}}
\newcommand{\cemph}[1]{\textcolor{Blue}{#1}}
\newcommand{\remph}[1]{\textcolor{Red}{#1}}
\newcommand{\uemph}[1]{\underline{#1}}
\newcommand{\mlstep}[1]{\twoheadrightarrow_{\underline{#1}}}
\newcommand{\lstep}[1]{\to_{\underline{#1}}}
\newcommand{\mstep}[1]{\twoheadrightarrow_{#1}}
\newcommand{\m}[2]{ \{\mu_{#1}\}_{#1 \in #2}} 
\newcommand{\M}[3]{\{#1_i \mapsto #2_i\}_{i \in #3}} 
\newcommand{\bm}[4]{
\{(#1_i:#2_i) \mapsto #3_i\}_{i \in #4}} 
\newcommand{\nil}[0]{\mathsf{nil}} 
\newcommand{\cons}[0]{\mathsf{cons}} 
\newcommand{\vecc}[0]{\mathsf{vec}} 
\newcommand{\suc}[0]{\mathsf{S}} 
\newcommand{\nat}[0]{\mathsf{Nat}} 
\newcommand{\ind}[0]{\mathsf{Ind}} 
\newcommand{\app}[0]{\mathsf{app}} 
\newcommand{\rec}[0]{\mathsf{rec}} 
\newcommand{\case}[0]{\mathsf{case}} 
\newcommand{\eq}[0]{\mathsf{Eq}} 
\newcommand{\add}[0]{\mathsf{add}} 
\newcommand{\cc}[0]{\mathbf{CC}} 

%% \newarrowfiller{dasheq} {==}{==}{==}{==}
%% \newarrow {Mapsto} |--->
%% \newarrow {Line} -----
%% \newarrow {Implies} ===={=>}
%% \newarrow {EImplies} {}{dasheq}{}{dasheq}{=>}
%% \newarrow {Onto} ----{>>}
%% \newarrow {Dashto}{}{dash}{}{dash}{>}
%% \newarrow {Dashtoo}{}{dash}{}{dash}{>>}

\include{seppp_annotated}
\mode<presentation>
{
  %\usetheme{Warsaw}
  % or ...
%gets rid of bottom navigation bars
%\setbeamertemplate{footline}[page number]{}

%gets rid of navigation symbols
\setbeamertemplate{navigation symbols}{}
\setbeamertemplate{footline}[frame number]
\usetheme{default}
%\usecolortheme[named=MyBlue]{structure}
%\setbeamercolor{background canvas}{bg=Base3}
%\setbeamercolor{normal text}{fg=Base00}

%\usetheme{Edinburgh}

%  \setbeamercovered{transparent}
  % or whatever (possibly just delete it)
}

\usepackage[english]{babel}
\usepackage[latin1]{inputenc}
\usepackage{times}
\usepackage[T1]{fontenc}
% Or whatever. Note that the encoding and the font should match. If T1
% does not look nice, try deleting the line with the fontenc.

\title[DTP13]
{Church Encoding with Dependent Type and Self Type}

\author{Peng Fu, Aaron Stump}

\institute[University of Iowa]
{  
  Dept. of Computer Science\\
  University of Iowa}
\date{\today}
%\date{May 22, 2013 }
% If you have a file called "university-logo-filename.xxx", where xxx
% is a graphic format that can be processed by latex or pdflatex,
% resp., then you can add a logo as follows:

% \pgfdeclareimage[height=0.5cm]{university-logo}{university-logo-filename}
% \logo{\pgfuseimage{university-logo}}



% Delete this, if you do not want the table of contents to pop up at
% the beginning of each subsection:
%\AtBeginSubsection[]
%{
%  \begin{frame}<beamer>
%    \frametitle{Outline}
%    \tableofcontents[currentsection,currentsubsection]
%  \end{frame}
%}


% If you wish to uncover everything in a step-wise fashion, uncomment
% the following command: 

%\beamerdefaultoverlayspecification{<+->}

\begin{document}

\begin{frame}[plain]
  \titlepage
\end{frame}

\begin{frame}
  \frametitle{Motivation}
  \begin{itemize}
  \item<1-> Church encoding in system $\mathbf{F}$.
   \item<2-> Dependent type theory.
    \item<3-> Primitive inductive data type. 
  \end{itemize}
\end{frame}

%% \begin{frame}[fragile]
%% \frametitle{Church Encoding}

%% \begin{itemize}

%% \item Church numerals

%% $\mathsf{Zero}\ := \lambda s.\lambda z.z$

%%   $\mathsf{One}\ := \lambda s.\lambda z.\yemph{s}\ z$
  
%%   $\mathsf{Two}\ := \lambda s.\lambda z.\cemph{s\ s}\ z$

%% \item Numeric Functions

%% $\mathsf{Succ}\ := \lambda n. \lambda s.\lambda z.s\ (n\ s\ z)$

%% $\mathsf{add}\ := \lambda n.\lambda m. n\ \mathsf{Succ}\ m$

%% $\mathsf{pred}\ := \lambda n. \lambda f.\lambda x.n\ (\lambda g.\lambda h.h\ (g\ f)) (\lambda u.x)\ (\lambda u.u)$
  
%% \end{itemize}
%% \end{frame}

\begin{frame}[fragile]
\frametitle{Church Encoding}


  \begin{itemize}

  \item<1-> Why not use Church encoded data? 
  \item<2-> Inefficiency to retrieve subdata. 
  \item<3-> Can not prove $0 \not = 1$(e.g. Calculus of Construction $\cc$ ). 
  \item<4-> Induction principle is not derivable(e.g. $\cc$). 
  \end{itemize}
\end{frame}

\begin{frame}[fragile]
\frametitle{Church Encoding: Inefficiency}
\begin{itemize}
\item Linear time to compute predecessor: 
  
 $\mathsf{pred}\ (\mathsf{Succ}\ \bar{n}) \underbrace{\leadsto ... \leadsto}_{\geq n+1} \bar{n} $

  \item ``Unintuitive'' predecessor function. 

    $\mathsf{pred}\ := \lambda n. \lambda f.\lambda x.n\ (\lambda g.\lambda h.h\ (g\ f)) (\lambda u.x)\ (\lambda u.u)$

    \item It is inherent to Church encodings. 
\end{itemize}

\end{frame}

\begin{frame}
  \frametitle{Underivability of $0 \not = 1$}
  

  \begin{itemize}
      \item Depends on the notion of contradiction. 
      \item Calculus of Construction: 
        \[
        \begin{array}{lll}
        x =_A y & :=  & \Pi C:A\to *. C \ x \to C \ y
        \\
        
        \bot & := & \Pi X:*.X
        
        \\
        
         0 =_{\nat} 1 \to \bot & := &
        
        (\Pi C: \nat \to *. C \ 0 \to C \ 1) \to \Pi X:*.X
          
        \end{array}
        \]

   \item $0 =_{\nat} 1 \to \bot$ is underivable in $\cc$. 
   \item $\vdash_{cc} t : 0 \not =_{\nat} 1$ implies $\vdash_{F} |t| : |0 \not =_{\nat} 1|$

   \item $|0 =_{\nat} 1 \to \bot | := \Pi C.(C \to C)\to \Pi X.X$ in $\mathbf{F}$.
  \end{itemize}
  
\end{frame}

\begin{frame}
  \frametitle{Underivability of $0 \not = 1$}
  

  \begin{itemize}
      \item A change of notion of contradiction.
      \item Calculus of Construction: 
        \[
        \begin{array}{lll}
        x =_A y & :=  & \Pi C:A\to *. C \ x \to C \ y 
        \\
        \yemph{$\bot$} & :=  & \Pi A:*. \Pi x:A. \Pi y:A . x =_{A} y
        \\
        0 =_{\nat} 1 \to \yemph{$\bot$} & := &  (\Pi C:\nat \to *. C \ 0 \to C \ 1) 
        \\
        
         & & \to (\Pi A:*. \Pi x:A. \Pi y:A . x =_{A} y)
        \end{array}
        \]
        \item \yemph{$\bot$} is uninhabited in $\cc$.
          \item $0 =_{\nat} 1 \to \yemph{$\bot$}$ is derivable in $\cc$.
          
   \item $0 \not = 1$ in $\cc$ is mapped to $\Pi C.(C \to C)\to (\Pi A. \Pi C. C \to C)$ in $\mathbf{F}$.
  \end{itemize}
\end{frame}

\begin{frame}
  \frametitle{Underivability of Induction Principle}
  \begin{itemize}
      \item Depends on the formulation of the logical system. 
      \item Calculus of Construction: 

        $Ind := \Pi P:\mathsf{Nat} \to *. (\Pi y:\mathsf{Nat}.(P y \to P(\mathsf{S} y))) \to P\ \bar{0} \to \Pi x:\mathsf{Nat}.P\ x$. 
        
       \item Let $\Gamma = P: \mathsf{Nat} \to *, s:\Pi y:\mathsf{Nat}.(P y \to P(\mathsf{S} y)), z:P\ \bar{0}, x:\nat$
         
         $ \Gamma \vdash ? : P\ x$
  
  \end{itemize}
\end{frame}

\begin{frame}
  \frametitle{Underivability of Induction Principle}

  $\Gamma = P: \mathsf{Nat} \to *, s:\Pi y:\mathsf{Nat}.(P y \to P(\mathsf{S} y)), z:P\ \bar{0}, x:\nat$
  \begin{itemize}
 \item<1-> Observe that: 
   
          $\Gamma \vdash z: P\ \bar{0}$

          $\Gamma \vdash s\ \bar{0}\ z: P\ \bar{1}$
   
          $\Gamma \vdash s\ \bar{1}\ (s\ \bar{0}\ z): P\ \bar{2}$

   \item<2-> A new notion of Lambda numerals: 

     $\yemph{$\bar{0}$} := \lambda s.\lambda z.z :$
     
     $(\Pi y:\mathsf{Nat}.(P y \to P(\mathsf{S} y))) \to P\ \bar{0} \to P\ \yemph{$\bar{0}$}$
     
     $\yemph{$\bar{1}$} := \lambda s.\lambda z. s\ 0\ z :$
     
     $ (\Pi y:\mathsf{Nat}.(P y \to P(\mathsf{S} y))) \to P\ \bar{0} \to P\ \yemph{$\bar{1}$}$
     
     $\yemph{$\bar{2}$} := \lambda s.\lambda z. s\ 1\ (s\ \bar{0}\ z) : $
     
     $ (\Pi y:\mathsf{Nat}.(P y \to P(\mathsf{S} y))) \to P\ \bar{0} \to P\ \yemph{$\bar{2}$}$
     
     $\suc := \lambda n.\lambda s.\lambda z. s\ n\ (n\ s\ z)$
   \item<3-> 
     
    $\nat := \Pi P:\mathsf{Nat} \to *. (\Pi y:\mathsf{Nat}.(P y \to P(\mathsf{S} y))) \to P\ \bar{0} \to P\ \yemph{$\bar{n}$}$ for every $\yemph{$\bar{n}$}$ ? 
  \end{itemize}
        
  
\end{frame}

\begin{frame}
\frametitle{Self Type: Introduction}
    $\nat := \Pi P:\mathsf{Nat} \to *. (\Pi y:\mathsf{Nat}.(P y \to P(\mathsf{S} y))) \to P\ \bar{0} \to P\ \yemph{$\bar{n}$}$ for every $\yemph{$\bar{n}$}$ ? 

\begin{itemize}
\item We introduce \textit{self} type. 
  
  \item $\nat := $
    
    $\yemph{$\iota x$}. \Pi P:\mathsf{Nat} \to *. (\Pi y:\mathsf{Nat}.(P y \to P(\mathsf{S} y))) \to P\ \bar{0} \to P \yemph{$x$}$

    
    \item Typing rules:
  \begin{tabular}{ll}
\infer[\textit{SelfInst}]{\Gamma \vdash t: [t/x]T}{\Gamma
\vdash t : \iota x.T}


&
\infer[\textit{SelfGen}]{\Gamma \vdash t : \iota x.T}{\Gamma
\vdash t: [t/x]T}
\\    
\end{tabular}
  \item Self type formation rule: 
    
    \begin{tabular}{l}
    \infer{\Gamma \vdash \iota x.T : *}{\Gamma, x:\iota x.T \vdash T: *}      
    \end{tabular}


\end{itemize}
\end{frame}

\begin{frame}
\frametitle{Self Type: Handling Recursive Definition}
$\remph{\nat} := $
    
    $\iota x. \Pi P:\remph{\mathsf{Nat}} \to *. (\Pi y:\remph{\mathsf{Nat}}.(P y \to P(\mathsf{S} y))) \to P\ \bar{0} \to P x$

\begin{itemize}
\item The encoding is not quite Church-like yet.

     $0 := \lambda s.\lambda z.z $
     
     $\suc := \lambda n.\lambda s.\lambda z. s\ \remph{n}\ (n\ s\ z)$
  
  \item We need Miquel's implicit product.
    
    $\remph{\nat} := $
    
    $\iota x. \Pi P:\remph{\mathsf{Nat}} \to *. (\yemph{$\forall$} y:\remph{\mathsf{Nat}}.(P y \to P(\mathsf{S} y))) \to P\ \bar{0} \to P x$

    \item Now we have Church numerals:
      
      $0 := \lambda s.\lambda z.z $
     
     $\suc := \lambda n.\lambda s.\lambda z. s\ (n\ s\ z)$
      \item Induction now is derivable: 
        
        $Ind : \Pi P:\mathsf{Nat} \to *. (\yemph{$\forall$} y:\mathsf{Nat}.(P y \to P(\mathsf{S} y))) \to P\ \bar{0} \to \Pi x:\mathsf{Nat}.P\ x$
        
        $Ind := \lambda s.\lambda z.\lambda n.n \ s\ z$.
  
    
\end{itemize}  
\end{frame}


\begin{frame}
\frametitle{Summary and Results}

\begin{itemize}
  \item  $0 \not =1$ is provable with a change of notion of contradiction.
\item Introduce Self type to derive induction principle.
\end{itemize}  

Some Results
\begin{itemize}
\item Self type is incorporated in a type system called $\mathbf{S}$. 
\item We prove $\mathbf{S}$ can be erased to $\mathbf{F}_{\omega}$, thus establishing consistency. 
\item We prove preservation theorem for $\mathbf{S}$.
\end{itemize}

\end{frame}

\begin{frame}
\frametitle{Thank you for listening!}

\begin{itemize}
\item Questions? 
\end{itemize}  
\end{frame}


\end{document}



